Masses Mass Genesis T10 Channel Cost Irreducibility Dof Pricing Unit Eq One Of I

The irreducible pricing unit

The declaration dofPricing_unit_eq_one_of_irreducible establishes a precise structural fact within the Recognition Science framework's mass-generation model. It states that if a pricing configuration p has a rung-per-degree-of-freedom value that is positive and irreducible, then that value must be exactly 1. Here, a positive integer is irreducible if it cannot be written as the sum of two smaller positive integers, which in this context means it is a minimal, indivisible unit of pricing. The theorem proves that the only such minimal unit is 1 itself, a fact that follows from the definition of irreducibility.

This result is not a physical measurement but a formal theorem about the framework's own definitions. It is proved in the machine-checked library of formal theorems, and it shows that the framework's notion of an irreducible pricing unit is uniquely fixed. The theorem also has a direct corollary: any irreducible pricing configuration is minimal among all positive pricing configurations, meaning no other configuration can have a smaller rung-per-degree-of-freedom value. This minimality is what allows the framework to build a stable foundation for its particle mass ladder, where the base pricing unit is always 1.

In Recognition Science, the framework models the cost of recognition through a specific function, and this cost is what ultimately determines particle masses. The theorem about the irreducible pricing unit is a key step in showing that the framework's mass-generation mechanism is internally consistent and that its fundamental unit is not arbitrary but forced by its own definitions. It does not, however, claim anything about the actual measured masses of particles; that comparison is an empirical check, not a theorem. The theorem is about the framework's internal logic, not about the physical world.

/-- **THEOREM (the irreducible pricing unit is `1`).** The per-axis rung unit
of an irreducible pricing is one rung. -/
theorem dofPricing_unit_eq_one_of_irreducible (p : DofPricing)
    (hirr : PosIrreducible p.rungPerDof) : p.rungPerDof = 1 :=
  (posIrreducible_iff_eq_one p.rungPerDof).1 hirr

/-- **THEOREM (irreducibility gives the minimal pricing).** An irreducible
pricing is below every nondegenerate pricing, recovering the hypothesis form
`DofPricing` closures consume. -/
theorem dofPricing_minimal_of_irreducible (p : DofPricing)
    (hirr : PosIrreducible p.rungPerDof) : ∀ q : DofPricing, p.rungPerDof ≤ q.rungPerDof := by
  intro q
  rw [dofPricing_unit_eq_one_of_irreducible p hirr]
  exact q.rungPerDof_pos

What this page does not claim

The theorem does not claim that the framework's pricing unit corresponds to any specific physical quantity or measured mass. The theorem does not claim that the framework's mass-generation model is physically correct; it only establishes internal consistency. The theorem does not claim that the notion of irreducibility is the only way to define a minimal pricing unit.

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/MassGenesis/T10ChannelCostIrreducibility.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: