Masses Dof Pricing Base Rule Of Minimal Pricing

The minimal pricing rule

The declaration base_rule_of_minimal_pricing is a result in the framework's machine-checked library. It states that if a pricing rule assigns to each degree of freedom an integer number of rungs, and that integer is the smallest possible nonzero integer, then the price of a two-sided channel is exactly 2 rungs. This result follows directly from two earlier facts: the minimal unit is 1, and a channel with two sides costs twice that unit.

The framework models a particle's mass as a position on a ladder of powers of the golden ratio. A pricing rule assigns to each independent degree of freedom a rung, an integer step on that ladder. The rule is homogeneous: two independent degrees of freedom cost twice the rung of one. The only freedom in the rule is the size of that single rung. The minimality principle selects the smallest possible rung, which is 1. A channel, defined as a distinction with exactly two sides, then costs 2 rungs. The result packages this as the base rule: the exponent 2 multiplies the number of active channel classes.

The result does not claim that the minimality principle is itself derived. It is a modeling choice, a principle selected because it is the only one that closes the rule. Without it, a rung of 2 is also nondegenerate, and it changes the coherence quantum observably: the exponent becomes 10 instead of 5. The result shows that minimality is the unique selection principle on the table, but it does not derive that principle from anything deeper.

In plain terms, the result pins down the base coefficient of the mass formula. The framework's account of particle masses rests on this coefficient, and the result establishes it as 2 rather than any other integer. The consequence is that the mass ladder's base step is fixed, and the framework's predictions for particle masses follow from that fixed step.

/-- **THEOREM (the base rule closes).** The minimal per-dof pricing plus the
banked two-sidedness forces the rung base rule, through
`RungBaseBoundary.channel_cost_premise_closes_base`. -/
theorem base_rule_of_minimal_pricing (p : DofPricing)
    (hmin : ∀ q : DofPricing, p.rungPerDof ≤ q.rungPerDof) (f : Fermion) :
    p.exponentOf 2 * activeChannelClasses f = 2 * activeChannelClasses f :=
  channel_cost_premise_closes_base (p.exponentOf 2)
    (base_coefficient_two_of_minimal p hmin) f

/-- A per-dof rung pricing: each configuration degree of freedom contributes
the same INTEGER rung unit (integrality banked by the ℤ-ladder; homogeneity is
the modeling content of "degree of freedom"), at least one rung
(nondegeneracy: a genuine dof is visible in the price, the same exclusion
`UnitFromMinimality` applies to the zero exponent). Independent dofs add
exponents by `dof_exponents_add`, so the only freedom in the rule is this one
integer. -/
structure DofPricing where
  rungPerDof : ℤ
  rungPerDof_pos : 1 ≤ rungPerDof

/-- **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

This result does not derive the minimality principle from deeper axioms; it is a modeling choice. This result does not state that a rung of 2 is impossible, only that it is not minimal and changes predictions. This result does not by itself produce a particle mass value; it fixes one coefficient in a larger formula.

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: