Research: effective scale-carrier ladder and surreal necessity gate #142

Context

Issue #140 and draft PR #141 reached a responsible NARROW result. The
registered raw-Bessel pipeline produces an exact local Newton/germ chart, but
the runtime uses only rational weights and finite analytic jets. Surreal
numbers motivated the scale-ensemble and kernel-opening semantics, yet were
neither an algorithmic dependency nor a uniquely necessary theorem carrier.

That result does not refute the surreal direction: the frozen Bessel task lies
entirely inside a finite polynomial/analytic regime and therefore cannot
discriminate among rational Newton weights, Hahn fragments, logarithmic-
exponential transseries, hyperseries, and the surreal field.

This issue opens a separate, falsifiable gate:

For which task families is each scale carrier sufficient, and what is the
first exact workload—if any—where a surreal or hyperserial carrier produces
a theorem, certificate, compression, or reachable computation unavailable
from a smaller effective carrier?

It authorizes a research-local Sonnet:

sonnet/effective-scale-carrier-ladder/

It does not authorize a general surreal runtime, Experimental/Public API, or
changes to the Mathematical Core.

Research target

Construct a carrier ladder compiler whose input is a frozen symbolic task
and whose output is one of:

minimum sufficient carrier + exact lowering/eliminability certificate
strict carrier-upgrade obstruction + witness
multiple incomparable task-relative carriers
inconclusive within a declared proof/search budget
outside the implemented grammar

Candidate levels begin conservatively:

C0  rational Newton weights / finite polynomial germs
C1  finite Hahn support / ordered monomial groups
C2  logarithmic-exponential transseries of finite construction height
C3  hyperserial / iterated-log-exp structure
C4  surreal semantic envelope with explicit effective shadow

The labels are provisional research-local types, not claims that these
categories have already been implemented or separated.

Central anti-hype theorem pressure

The first mathematical question is eliminative:

Does every finite expression DAG generated by rational constants,
algebraic operations, exp, and log, under a finite observation task,
lower to a finite-height LE-transseries fragment?

If yes, then full surreal arithmetic is unnecessary for that entire grammar.
This is a positive result: the compiler should return an exact
surreal-eliminable certificate rather than instantiate a larger carrier.

Surreal necessity may be credited only after this smaller-carrier baseline
fails for a frozen task.

First discriminating workload family

Use three strata.

L0 — finite control

Reuse the Bessel local germ from #140. The correct minimum carrier is C0. Any
system that promotes it to surreal fails minimality.

L1 — finite nested exp/log family

Freeze expressions of increasing but finite construction height. Measure
normal-form size, comparison cost, observer lowering, and certificate growth.
The expected null hypothesis is C2 sufficiency with no surreal runtime need.

L2 — iteration/Abel gate

Study a declared local/asymptotic task around the functional equation

[
F(x+1)=\exp(F(x)),
]

together with the inverse/logarithmic iteration where well typed. Fixed finite
iterates receive zero evidence for C3/C4; the task must ask for a uniform
symbolic-height law, an iteration normal form, or another property that cannot
be obtained by merely unrolling a fixed integer height.

The gate must distinguish:

• a true hyperserial construction;
• a surreal field used only as a large ambient set;
• a finite effective shadow that can be computed and independently replayed;
• unresolved existence, branch, normalization, or uniqueness assumptions.

Software deliverable

Implement only the smallest visible artifact:

• a backend-neutral ScaleExpr/carrier-feature IR;
• exact feature and construction-height extraction;
• carrier-capability declarations;
• lowering/upgrade obligations;
• deterministic CarrierDecisionCertificate;
• typed refusal when a claimed carrier lacks closure or comparison;
• corpus runner and cost ledger.

Python/SymPy owns the changing grammar. No Rust or full surreal-number
implementation is justified before the certificate schema stabilizes and a
measured kernel appears.

Three parallel workstreams

A — mathematics and literature

1. Define the carrier ladder without false inclusions or vocabulary collapse.
2. Prove the strongest finite-grammar eliminability result available.
3. Audit Abel/tetration, transseries, hyperseries, and surreal embedding/
   extension results using primary sources.
4. Identify exact existence, uniqueness, normalization, and effectiveness
   gaps.
5. Supply a candidate separation theorem or a proof that the proposed gate
   still cannot distinguish C3 from C4.

B — compiler

1. Freeze the IR, carrier capabilities, obligations, budgets, and certificate.
2. Implement C0–C2 feature inference and lowering evidence.
3. Represent C3/C4 as explicit unsupported/conditional capabilities until
   mathematics and execution justify them.
4. Pass L0 and held-out finite-height controls without carrier overpromotion.
5. Expose certificate size and compilation/replay costs.

C — red team and baselines

1. Freeze same-information tasks before compiler tuning.
2. Compare SymPy, available transseries/asymptotic tooling, and executable
   systems where actually available.
3. Detect hidden unrolling, answer leakage, ambient-set masquerading, and
   non-effective certificates.
4. Require at least one negative/minimality result and one correct refusal.
5. Independently replay every positive carrier decision.

Evidence firewall

Before implementation, freeze:

• the task grammar and observer;
• carrier capability matrix;
• positive, negative, and held-out cases;
• what counts as a lowering certificate;
• maximum construction height and resource budget;
• the rule separating fixed-height verification from symbolic-height
  discovery;
• exact claim words for sufficient, necessary, minimal, effective,
  and surreal.

No carrier may receive credit merely because an expression embeds into it.

Disposition

Publish exactly one outcome:

• ELIMINATE: the frozen workloads all lower to smaller effective carriers;
  surreal remains a semantic envelope, not a runtime dependency.
• EXPAND: a frozen task has a replayable smaller-carrier obstruction and a
  surreal/hyperserial effective certificate or workload advantage.
• NARROW: the carrier ladder and software artifact are useful, but the
  C3/C4 boundary or effectiveness claim remains unresolved.
• STOP: the distinction is terminology, hidden unrolling, unsupported
  embedding, or uneconomic residual state.

Acceptance criteria

• Carrier levels and inclusion/closure claims are source-audited.
• Finite DAG, finite task, and symbolic-height tasks are separated.
• L0 returns C0 without overpromotion.
• At least one nontrivial finite-height family returns an exact lowering
  certificate and cost curve.
• Abel/iteration assumptions and normalization are explicit.
• No fixed iterate is reported as symbolic-height discovery.
• At least one unsupported C3/C4 request fails with a typed obligation.
• Every positive result has an independent replay.
• Certificate, compilation, replay, residual, and decoder costs are
  separated.
• The strongest claim is no broader than the evidence.

Kill conditions

Narrow, eliminate, or stop if:

• full surreal arithmetic is introduced before a smaller carrier fails;
• finite exp/log syntax is relabeled as surreal without a new capability;
• an embedding theorem is treated as an effective algorithm;
• a fixed-height unrolling is treated as uniform iteration;
• Abel/tetration existence or normalization is hidden in an oracle;
• the certificate stores the full source trace without compression;
• a smaller transseries/hyperseries fragment supplies the same certificate at
  equal or lower total cost;
• no software-visible task or proof obligation changes.

Claim ceiling

This issue does not claim:

• that surreal numbers are necessary for analysis or Process Geometry;
• a canonical surreal tetration or hyperseries implementation;
• post-manifold geometry, Arithmetic Universality, or effective V5 closure;
• a complexity breakthrough or leverage on 3D Ising;
• replacement of standard numerical/symbolic analysis;
• any Experimental or Public API.

Initial status:

Epistemic maturity: T0 contract
Role: discriminating carrier/minimality gate
Code status: Sonnet-local
Claim mode: exact symbolic + bounded search

Governance

• Mathematical Core: unchanged.
• Research Programme: pressure on U1, U2, and E; no universality promotion.
• Research Status: unchanged at creation.
• Engineering Architecture: opens a research-local carrier decision and
  certificate stage.
• Theory Map: local pressure on filtered asymptotic fibres and task-
  covariant presentation; no stable node.
• Public API: none.