Masses Dof Pricing Ecoh Differs Without Minimality

The role of minimality

In the Recognition Science framework, particle masses are not arbitrary numbers. They are placed on a ladder of powers of the golden ratio, and the framework's library of machine-checked theorems derives this structure from a single cost function. The declaration ecoh_differs_without_minimality is a formal proof about what happens to this ladder when a key assumption is removed. It establishes that two different pricing rules, one where each degree of freedom costs one rung and one where it costs two, produce different coherence quanta. The proof shows that phi raised to the power of two times five is not equal to phi raised to the power of one times five. This is a precise, formal statement that the two scales are genuinely distinct.

The statement is a boundary condition, not a positive result. It does not prove that the two-rung pricing is correct, nor does it prove that the one-rung pricing is correct. It only proves that they are different. The framework's own derivation of the one-rung rule relies on a separate principle called minimality, which selects the smallest possible nondegenerate unit. The theorem ecoh_differs_without_minimality shows that without this principle, the framework's predictions are not unique. A second nondegenerate unit exists, and it changes the observable predictions of the model. The theorem therefore marks the exact point where a modeling choice, not a mathematical necessity, enters the framework.

What the declaration does not claim is as important as what it proves. It does not claim that the two-rung pricing is a valid alternative that fits any data. It does not claim that minimality is false. It does not claim that the framework fails without minimality; it claims the opposite, that the framework's uniqueness is contingent on that principle. The theorem is a precise measurement of the boundary of the framework's derivational power. It tells a reader exactly where the mathematics stops and the modeling assumptions begin. This is the kind of honesty that makes the framework's larger claims testable, because it names the specific principle that carries the weight.

/-- **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 prove that the two-rung pricing is physically correct. The theorem does not prove that the minimality principle is false. The theorem does not show that the framework's predictions are wrong without minimality, only that they are not unique.

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: