structure definition def or abbrev high

`of`

The structure of bundles the factorization property on the positive reals under multiplication with the calibrated J-cost. Researchers deriving the Recognition Composition Law from ledger axioms cite it as the interface between substitutivity and the RCL. The definition directly assembles contextual substitutivity and regrouping invariance into a single object.

claimLet $G = (ℝ_+, ×)$ be the positive reals under multiplication equipped with the J-cost calibration. The structure of consists of contextual substitutivity (replacing any subcomparison by a cost-equivalent one leaves total cost unchanged) together with regrouping invariance (cost of any triple comparison is independent of parenthesization).

background

The module derives the factorization property, and hence the Recognition Composition Law, from two primitive ledger axioms. Contextual substitutivity requires that cost-equivalent replacements inside a comparison do not alter the total J-cost. Regrouping invariance requires that the J-cost of a triple comparison is independent of parenthesization. These two properties together force the combiner to satisfy the FactorizationAssociativityGate, after which gate_forces_rcl yields the RCL polynomial exactly. Upstream results include the structure of J-cost from PhiForcingDerived.of, the spectral emergence of gauge content and generations from SpectralEmergence.of, and the external calibration map from SingleAnchor.calibration.

proof idea

As a definition the construction is a direct packaging of the two supplied properties into one structure. No lemmas are invoked inside the body; the object is simply the pair of contextual substitutivity and regrouping invariance, ready for use by ledger_forces_rcl and downstream theorems.

why it matters in Recognition Science

This definition supplies the missing link from the two ledger primitives to the RCL, which is then consumed by energyConservationCert, costRateEL_const_one, and the full suite of Euler-Lagrange results. It occupies the precise step in the foundation chain that converts substitutivity and invariance into the composition law required for the forcing sequence T5–T8. The declaration therefore closes one segment of the path from the single functional equation to the observed constants and dimensions.

scope and limits

Does not itself prove the RCL polynomial; that step is performed by gate_forces_rcl.
Does not supply numerical values for constants such as alpha or G.
Does not extend the factorization property beyond the positive reals under multiplication.
Does not incorporate the eight-tick octave or spatial dimension forcing.

formal statement (Lean)

  42structure of `(ℝ₊, ×)` and the calibration of `J`. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

srCost_pos_off_threshold in IndisputableMonolith.Acoustics.SpeechIntelligibilityFromJCost decl_use
applied in IndisputableMonolith.Action.EnergyConservationDomainCert decl_use
energyConservationCert in IndisputableMonolith.Action.EnergyConservationDomainCert decl_use
christoffel in IndisputableMonolith.Action.EulerLagrange decl_use
const_one_is_geodesic in IndisputableMonolith.Action.EulerLagrange decl_use
costRateEL_const_one in IndisputableMonolith.Action.EulerLagrange decl_use
costRateEL_iff_const_one in IndisputableMonolith.Action.EulerLagrange decl_use
costRateEL_implies_const_one in IndisputableMonolith.Action.EulerLagrange decl_use
geodesicEquationHolds in IndisputableMonolith.Action.EulerLagrange decl_use
geodesic_iff_hessianEnergy_EL in IndisputableMonolith.Action.EulerLagrange decl_use
hessianMetric_eq in IndisputableMonolith.Action.EulerLagrange decl_use
actionJ_convex_on_interp in IndisputableMonolith.Action.FunctionalConvexity decl_use
actionJ_local_min_is_global in IndisputableMonolith.Action.FunctionalConvexity decl_use
actionJ_minimum_unique_value in IndisputableMonolith.Action.FunctionalConvexity decl_use
geodesic_minimizes_unconditional in IndisputableMonolith.Action.FunctionalConvexity decl_use
Jcost_convex_combination in IndisputableMonolith.Action.FunctionalConvexity decl_use
energy_conservation in IndisputableMonolith.Action.Hamiltonian decl_use
hamilton_equations_from_EL in IndisputableMonolith.Action.Hamiltonian decl_use
totalEnergy in IndisputableMonolith.Action.Hamiltonian decl_use
newtonSecondLawCert in IndisputableMonolith.Action.NewtonSecondLawDomainCert decl_use
space_translation_invariance_implies_momentum_conservation in IndisputableMonolith.Action.Noether decl_use
actionJ_def in IndisputableMonolith.Action.PathSpace decl_use
actionJ_nonneg in IndisputableMonolith.Action.PathSpace decl_use
const_apply in IndisputableMonolith.Action.PathSpace decl_use
Jcost_quadratic_leading_coeff in IndisputableMonolith.Action.QuadraticLimit decl_use
Jcost_taylor_quadratic in IndisputableMonolith.Action.QuadraticLimit decl_use
standardEL in IndisputableMonolith.Action.QuadraticLimit decl_use
comma_small in IndisputableMonolith.Aesthetics.MusicalScale decl_use
scale_fibonacci in IndisputableMonolith.Aesthetics.MusicalScale decl_use
twelve_from_phi in IndisputableMonolith.Aesthetics.MusicalScale decl_use

… and 10 more

depends on (6)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
calibration in IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use