Masses Dof Pricing Ecoh Exponent Eq Config Dim

The coherence exponent

The declaration ecoh_exponent_eq_configDim is a theorem in the framework's machine-checked library of formal theorems. It states: under a pricing rule where each independent degree of freedom contributes the same integer rung unit, and where that unit is the least possible nondegenerate one, the coherence exponent of a configuration equals the configuration dimension itself. In the specific case where the configuration dimension is 3, the theorem derives that the coherence exponent is 5.

The ledger, a discrete record of events, assigns each configuration degree of freedom a rung on a phi-power ladder. The pricing rule multiplies ratios; exponents add when factors are independent. The theorem's proof uses the fact that the minimal unit is exactly 1, so the exponent of a configuration with dimension d is simply d. With the configuration dimension set to 3, the exponent becomes 5.

This theorem does not claim that the configuration dimension is 3. That value comes from a separate derivation in the foundation library, GapDerivation. The theorem also does not claim that the minimality principle is forced by the framework's axioms. Minimality is a selection principle, a modeling choice, not a theorem. Without it, a nondegenerate unit of 2 exists, and the coherence exponent becomes 10, not 5, a difference the framework proves is observable.

In Recognition Science, this result recovers a modeling step from earlier work: it shows that the coherence exponent matches the configuration dimension under the minimal pricing rule. The theorem's value is that it makes the connection precise and machine-checked. It does not, by itself, establish the physical bridge from recognition to linking, which remains an open target.

/-- **THEOREM (B-22's modeling step recovered).** Under the minimal pricing
the coherence exponent is the configuration dimension itself: with
`configDim 3 = 5` (`Foundation/GapDerivation.lean`), the exponent is 5. -/
theorem ecoh_exponent_eq_configDim (p : DofPricing)
    (hmin : ∀ q : DofPricing, p.rungPerDof ≤ q.rungPerDof) :
    p.exponentOf (Foundation.GapDerivation.configDim Foundation.GapDerivation.D) = 5 := by
  have hu := DofPricing.unit_eq_one_of_minimal p hmin
  simp [DofPricing.exponentOf, hu, Foundation.GapDerivation.configDim,
    Foundation.GapDerivation.D]

/-- **THEOREM (B-22's modeling step recovered).** Under the minimal pricing
the coherence exponent is the configuration dimension itself: with
`configDim 3 = 5` (`Foundation/GapDerivation.lean`), the exponent is 5. -/
theorem ecoh_exponent_eq_configDim (p : DofPricing)
    (hmin : ∀ q : DofPricing, p.rungPerDof ≤ q.rungPerDof) :
    p.exponentOf (Foundation.GapDerivation.configDim Foundation.GapDerivation.D) = 5 := by
  have hu := DofPricing.unit_eq_one_of_minimal p hmin
  simp [DofPricing.exponentOf, hu, Foundation.GapDerivation.configDim,
    Foundation.GapDerivation.D]

/-- **THEOREM (non-minimal pricings change the coherence quantum).** At unit
2 the coherence exponent is 10, not 5, and the ladder is injective, so the
two coherence quanta differ. -/
theorem ecoh_differs_without_minimality :
    phi ^ ((2 : ℤ) * 5) ≠ phi ^ ((1 : ℤ) * 5) := by
  intro h
  have h' := Constants.PhiLadder.rung_of_value_unique h
  omega

What this page does not claim

The theorem does not establish that the configuration dimension is 3. The theorem does not prove the minimality principle from the framework's axioms. The theorem does not bridge recognition events to physical linking.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Masses/DofPricing.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: