IndisputableMonolith.Foundation.SubstitutivityForcing
The SubstitutivityForcing module shows that the cost_sufficient field inside ZeroParameterComparisonLedger supplies contextual substitutivity with no separate axiom required. Researchers building the unconditional inevitability theorem cite it to justify substitution inside the ledger. The argument is a direct extraction from the ledger definition imported from LedgerCanonicality.
claimThe cost_sufficient field of ZeroParameterComparisonLedger directly yields contextual substitutivity: given states with symmetric local cost and conserved log-charge, substitution holds in the comparison without extra hypotheses.
background
The module sits in the Foundation domain and imports LedgerCanonicality, whose ZeroParameterComparisonLedger packages a countable carrier for discrete states, a symmetric cost on local binary comparisons, and a conserved log-charge scalar. The upstream doc-comment states that this ledger is the refined primitive object for the unconditional inevitability theorem.
SubstitutivityForcing extracts the substitution property from the cost_sufficient component of that ledger. No new structure is added; the module simply records that the existing field already encodes the needed contextual replacement rule.
proof idea
This is a theorem module whose core result, substitutivity_from_ledger, follows immediately from the cost_sufficient field of the imported ledger definition. The remaining siblings (lambda_one_is_unique_fixpoint, calibration_forced_from_fixpoint) are one-line wrappers that apply the same field to fixpoint and calibration statements.
why it matters in Recognition Science
The module removes an extra axiom from the forcing chain that leads to the unconditional inevitability theorem. By confirming that substitutivity is already present in the ledger, it lets the T5 J-uniqueness and T6 phi fixed-point steps proceed directly. The doc-comment explicitly notes that no additional axiom is needed.
scope and limits
- Does not define ZeroParameterComparisonLedger or its cost_sufficient field.
- Does not treat global rather than local conservation.
- Does not supply numerical values for phi, alpha, or other constants.
- Does not extend the ledger to continuous or non-countable carriers.