structuralStratificationCertificate_holds

This module sits in the Primitive Recognition Calculus native-cost ledger. Costs are maps on the ratio-orbit carrier (quotients of positive ratios under reciprocal identification). The structural ledger is a slim hypothesis package that never names the canonical cost in two of its four fields, yet is meant to force that cost uniquely.

StructuralStratificationCertificate is the free-side packaging of that claim: uniqueness of the structural native cost, contraction of structural hypotheses to the zero-calibrated signed strengthened package, derived positivity, an inhabited infinite gauge orbit, gauge rigidity, and a non-vacuous witness. Upstream, PRCStructuralNativeCostUniquenessTarget_proved is the Round 5 terminal: the structural ledger forces the canonical cost via character factorization and cross-equation respect. Continuum comparisons (continuum_gauge_exceeds_native_gauge, continuum_monotone_class_is_the_scale_family) show that the real line admits a full positive-exponent scale family, while the carrier refutes even exponents and keeps only the odd-power orbit.

The local setting is the free (countable) side of native-cost uniqueness, before continuum completion reintroduces continuous scale freedom.

The proof is a structure constructor, not a fresh argument. It fills each field of StructuralStratificationCertificate by an already-proved (or stubbed) sibling:

• uniqueness from PRCStructuralNativeCostUniquenessTarget_proved (character factorization plus calibration on positive integers).
• contracts_slim from structural_forces_slim.
• positivity from structural_forces_positive.
• gauge_inhabited from the refutation PRCStructuralSansAnchorUniquenessTarget_refuted (sans-anchor uniqueness fails, so the gauge is non-trivial).
• gauge_orbit_infinite from gauge_orbit_contains_every_odd_power.
• gauge_rigid by wrapping structural_gauge_rigidity on matching monotone/character/factor data.
• nonvacuous from canonicalSelectedNativeCost_structural_hypotheses.

No new algebra is done here; discharge depends on the axiom audit of those leaves.

This is the free-side stratification receipt for the PRC native cost: arithmetic on the countable carrier forces the cost form, leaving only an anchor for unit size. That matches the Recognition Composition Law and J-uniqueness (T5) story, where the continuum scale family is larger than what the carrier admits (even powers refuted; odd powers present). The certificate is the single Prop a downstream uniqueness or minimality argument would cite instead of re-assembling seven lemmas.

No used_by edges are recorded yet, so it is presently a terminal packaging theorem inside the structural ledger module. The module's axiom audit explicitly #print axioms this declaration alongside the uniqueness, gauge-orbit, and continuum-comparison results, so any claim resting on the file is honest about sorryAx until the stubs close. Framework-wise it separates native (countable) forcing from continuum completion, the same split that keeps phi-ladder and eight-tick structure from being smuggled in as continuous scale freedom.