Masses Dof Pricing Dof Exponents Add

The ladder rule

The Recognition Science framework models particle masses as positions on a ladder of powers of the golden ratio phi. The declaration dof_exponents_add establishes the basic arithmetic of that ladder: multiplying two powers gives a power whose exponent is the sum, phi^a * phi^b = phi^(a+b). This is the standard law of exponents, here applied to the specific base phi. The theorem is proved for all integer exponents, positive, negative, and zero, and it holds without any additional assumptions about the physics. It is a pure statement about the algebraic structure of the ladder.

The declaration does not, by itself, claim anything about which particles exist, what their masses are, or how many degrees of freedom any particular system has. It establishes only the combining rule for independent factors. The framework's pricing rule, which assigns an integer rung to each degree of freedom, is a separate modeling choice. The exponent of a system with d independent degrees of freedom is defined as the product of that integer and d. The additivity theorem ensures that this product rule is consistent: independent factors combine by adding their exponents, as the ladder requires.

The theorem also does not select a particular value for the rung unit. A structure called DofPricing allows any positive integer as the rung per degree of freedom. A separate minimality principle, not this theorem, forces that unit to be 1. The additivity law is the algebraic backbone; the minimality principle is the economic one. They are distinct claims, and the additivity theorem does not imply the minimality result.

/-- **THEOREM (banked additivity).** Ratios on the ladder multiply; exponents
add. An event made of independent factors at ladder steps `a` and `b` sits at
step `a + b`. No premise: this is the zpow law on the φ-ladder. -/
theorem dof_exponents_add (a b : ℤ) : phi ^ a * phi ^ b = phi ^ (a + b) :=
  (zpow_add₀ (ne_of_gt phi_pos) a b).symm

What this page does not claim

No claim that any particular particle exists or has a specific mass. No claim that the rung unit must be 1; that is a separate minimality principle. No claim about the number of degrees of freedom of any physical system.

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: