Encyclopedia Masses Masses Dof Pricing Dof Pricing Boundary Without Minimality

ARTICLE 4 claims 4 theorems

Masses Dof Pricing Dof Pricing Boundary Without Minimality

A machine-checked theorem shows what happens if you drop the one selection principle in the framework's pricing rule: the predictions change.

Verify this page

The boundary without minimality

The framework's ledger, a discrete record of events, assigns each configuration degree of freedom an integer rung on a phi-power ladder. The pricing rule says independent degrees of freedom add their rung exponents, and the only freedom in the rule is that one integer: the rung per degree of freedom. The minimal choice, rung 1, is the one that recovers the framework's known coherence exponent 5 and base coefficient 2. But the rule itself does not force that choice. The theorem dofPricing_boundary_without_minimality packages what happens if you drop the minimality principle.

Without minimality, a second nondegenerate unit exists: rung 2 is still a valid per-degree-of-freedom price. That changes the coherence quantum observably: at rung 2 the coherence exponent is 10, not 5, and the two ladder values differ because the ladder is injective. The theorem also shows that at the rung table, the coefficient-4 deformation meets every banked clause while changing predictions. In plain terms, the framework's pricing rule alone does not select a unique unit; you need an extra principle to pin it down.

That extra principle is minimality, and the theorem is explicit that minimality is a principle, not a theorem. It is a modeling choice: among all nondegenerate pricings, take the least unit. The theorem proves that under that choice the coherence exponent and base coefficient recover their known values, and it proves that without the choice the predictions change. It does not prove that minimality is true, only that it is the selection principle that closes the rule.

What the declaration does not claim is as important as what it proves. It does not claim that rung 2 is forbidden by the pricing rule; the theorem shows rung 2 satisfies every banked clause. It does not claim that minimality is the only possible selection principle, only that it is the one on the table. And it does not claim that the predictions at rung 2 are wrong; it claims they differ. The boundary is a precise statement of what the framework can and cannot force without an extra assumption.

THEOREM dofPricing_boundary_without_minimality · IndisputableMonolith/Masses/DofPricing.lean
dofPricing_boundary_without_minimality · IndisputableMonolith/Masses/DofPricing.lean:139 
/-- **THEOREM (the boundary, packaged).** Without the minimality principle:
a second nondegenerate unit exists (2 ≥ 1), it changes the coherence quantum
observably, and at the rung table the coefficient-4 deformation meets every
banked clause while changing predictions. Minimality is the only selection
principle on the table, and it is a principle, not a theorem. -/
theorem dofPricing_boundary_without_minimality (Z : ℤ) :
    (1 ≤ (2 : ℤ))
    ∧ phi ^ ((2 : ℤ) * 5) ≠ phi ^ ((1 : ℤ) * 5)
    ∧ (∀ f : Fermion,
        shiftedRungs 2 f
          = (2 + 2) * activeChannelClasses f + Integers.tau (genOf f).val
            + (if f = Fermion.nu3 then 2 else 0))
    ∧ predictAt .Lepton (deformedTotal 2 Fermion.e) Z
        ≠ predictAt .Lepton (deformedTotal 0 Fermion.e) Z :=
  ⟨by norm_num, ecoh_differs_without_minimality,
    channel_cost_independent_without_premises Z⟩
THEOREM ecoh_differs_without_minimality · IndisputableMonolith/Masses/DofPricing.lean
ecoh_differs_without_minimality · IndisputableMonolith/Masses/DofPricing.lean:130 
/-- **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
THEOREM dofPricing_boundary_without_minimality · IndisputableMonolith/Masses/DofPricing.lean
dofPricing_boundary_without_minimality · IndisputableMonolith/Masses/DofPricing.lean:139 
/-- **THEOREM (the boundary, packaged).** Without the minimality principle:
a second nondegenerate unit exists (2 ≥ 1), it changes the coherence quantum
observably, and at the rung table the coefficient-4 deformation meets every
banked clause while changing predictions. Minimality is the only selection
principle on the table, and it is a principle, not a theorem. -/
theorem dofPricing_boundary_without_minimality (Z : ℤ) :
    (1 ≤ (2 : ℤ))
    ∧ phi ^ ((2 : ℤ) * 5) ≠ phi ^ ((1 : ℤ) * 5)
    ∧ (∀ f : Fermion,
        shiftedRungs 2 f
          = (2 + 2) * activeChannelClasses f + Integers.tau (genOf f).val
            + (if f = Fermion.nu3 then 2 else 0))
    ∧ predictAt .Lepton (deformedTotal 2 Fermion.e) Z
        ≠ predictAt .Lepton (deformedTotal 0 Fermion.e) Z :=
  ⟨by norm_num, ecoh_differs_without_minimality,
    channel_cost_independent_without_premises Z⟩
THEOREM ecoh_exponent_eq_configDim · base_coefficient_two_of_minimal · IndisputableMonolith/Masses/DofPricing.lean
ecoh_exponent_eq_configDim · IndisputableMonolith/Masses/DofPricing.lean:99 
/-- **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]
base_coefficient_two_of_minimal · IndisputableMonolith/Masses/DofPricing.lean:109 
/-- **THEOREM (the base coefficient recovered).** Under the minimal pricing,
a channel's two-sided dof count (premise P2: one channel is one distinction,
and a distinction has exactly two sides, `Foundation/BoolFromLogic.lean`)
prices at 2 rungs. -/
theorem base_coefficient_two_of_minimal (p : DofPricing)
    (hmin : ∀ q : DofPricing, p.rungPerDof ≤ q.rungPerDof) :
    p.exponentOf 2 = 2 := by
  have hu := DofPricing.unit_eq_one_of_minimal p hmin
  simp [DofPricing.exponentOf, hu]

What this page does not claim

Rung 2 is forbidden by the pricing rule. Minimality is the only possible selection principle. Predictions at rung 2 are empirically wrong.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND