realCharacterFactorizationHypotheses_of_structural

In the cost layer, native costs act on ratio orbits (equivalence classes of positive rational ratios from the primitive recognition calculus). The structural ledger PRCStructuralNativeCostHypothesesSansAnchor packages the full anchor-free native-cost axioms: a base without the distinguished two-point (reciprocal automorphism, normalized invariance, canonical Recognition Composition Law, unit zero), plus sign-reversal, monotonicity, and zero-calibration of the doubled trace.

SansAnchorHypotheses is the deliberately lighter pack that RealCharacterFactorization takes as input. Its doc states it is the "anchor-free pack matching" the structural ledger. The base-sans-two component reuses reciprocal and RCL structure from the cost algebra; sign-reversing and monotone are the usual comparison axioms; zero-calibrated means the doubled native-cost trace vanishes at the unit.

This module sits between the structural PRC ledger and the real-character factorization theorems that classify gauge orbits of costs.

Pure structure construction, no arithmetic. Build SansAnchorHypotheses F by projecting each field from the structural hypothesis hF:

• base_sans_two is assembled from hF.base_sans_two by copying reciprocal, normalized_invariant, canonical_rcl, and unit_zero.
• sign_reversing is hF.sign_reversing applied pointwise.
• monotone is discharged by intro on the order hypotheses and calling hF.monotone.
• zero_calibrated is exactly hF.zero_calibrated.

No lemmas beyond field access; the two packs are definitionally aligned on these components.

This is the import bridge that lets every structural anchor-free cost inherit the real factorization proved in RealCharacterFactorization. Downstream, structural_sansAnchor_realCharacterFactorization quotes it to obtain a real ratio character $\chi$ with the native cost recovered from $\chi$; its doc says "Every structural anchor-free cost has the real factorization proved in RealCharacterFactorization."

Further downstream, GaugeOrbitIsSignedPowerFamily_of_sixExponentials applies it as the first step (have hS := realCharacterFactorizationHypotheses_of_structural hG) before case-splitting on the rational trace at 2, yielding the anchor-free gauge classification: every such cost is the sign cost or a sign-extended power cost of a nonnegative integer exponent (under the six-exponentials input). That classification is the cost-side input to selecting $J$ by leastness elsewhere; it does not itself force $J$ or odd exponents.

In the forcing chain this sits under cost uniqueness and the RCL, not under T5–T8 directly, but it is how structural ledgers enter the gauge-orbit story.