Encyclopedia Masses Masses Mass Genesis T10 Yardstick Premise Free Cert Ew Wallpaper Content Eq Deri

ARTICLE 2 claims 2 theorems

Masses Mass Genesis T10 Yardstick Premise Free Cert Ew Wallpaper Content Eq Deri

A theorem in the Recognition Science framework shows that a key electroweak number can be derived from structure alone, not assumed.

Verify this page

The wallpaper identity

The declaration ew_wallpaper_content_eq_derived_cellReach_mul_W is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It states that the electroweak wallpaper content, defined as the banked electroweak yardstick minus twice the derived channel reach, equals the derived cell reach multiplied by the top-generation torsion W. In plainer terms, it says that a certain structural quantity, the wallpaper content, is exactly the product of two other derived quantities: the cell reach and the torsion value. The theorem is part of a larger certificate that aims to show the number 55, a yardstick used in the framework's mass-genesis model, arises from the derivation chain rather than from a frozen stipulation.

To understand what this means, it helps to know the framework's vocabulary. The ledger, a discrete record of events, is used to price couplings between particles. The cell reach is the number of inhabited cells a coupling touches, and the channel reach is the number of distinct species channels it spans. The theorem itself is a formal identity: it rewrites the definition of the derived yardstick and uses the fact that the cell reach of the derived W coupling is 3. It does not, by itself, prove that the cell reach is 3 or that the yardstick is 55; those are separate theorems in the same file. What this specific theorem establishes is the algebraic relationship between the wallpaper content, the cell reach, and the torsion W, given those other results.

The theorem is notable because it is part of a "premise-free" certificate. This means the derivation does not rely on the banked definition of the yardstick as a premise; the value 55 is computed from the derived reaches and the wallpaper count. The theorem also helps exclude a "decoy" reading: pricing three inhabited cells at two rungs each gives 57, not 55, and this theorem is used to show why the correct reading is the wallpaper content, not the cell reading. In the framework's account, this is a step toward showing that the electroweak structure is forced by the recognition-cost logic, not chosen.

What this declaration does not claim is equally important. It does not claim that the electroweak yardstick is 55; that is a separate theorem. It does not claim that the cell reach is 3 or that the channel reach is 2; those are also separate results. It does not claim anything about the physical mass of any particle, nor does it claim that the framework's model matches experimental data. The theorem is a purely formal identity within the framework's own definitions. It is a piece of the larger argument, not the argument itself.

THEOREM ew_wallpaper_content_eq_derived_cellReach_mul_W · IndisputableMonolith/Masses/MassGenesis/T10YardstickPremiseFreeCert.lean
ew_wallpaper_content_eq_derived_cellReach_mul_W · IndisputableMonolith/Masses/MassGenesis/T10YardstickPremiseFreeCert.lean:184 
/-- **THEOREM (C14 wallpaper identity, derived form).** The electroweak
wallpaper content (`r0(EW)` minus the channel-reach offset) IS the derived
cell reach times `W`. -/
theorem ew_wallpaper_content_eq_derived_cellReach_mul_W :
    Anchor.r0 Anchor.Sector.Electroweak - 2 * channelReach derivedWCouples
      = cellReach derivedWCouples * (Anchor.W : ℤ) := by
  rw [anchor_r0_ew_eq_derivedEWYardstick]
  unfold derivedEWYardstick
  ring
THEOREM yardstick_premise_free_certificate · IndisputableMonolith/Masses/MassGenesis/T10YardstickPremiseFreeCert.lean
yardstick_premise_free_certificate · IndisputableMonolith/Masses/MassGenesis/T10YardstickPremiseFreeCert.lean:268 
/-- **THE C16 CROWN: the premise-free 55 certificate.** One proposition:

1. VALUE: the banked yardstick IS the derived structure, whose value is
   `55` (the agreement bridge plus the cone-clean computation);
2. CELL COUNT FORCED: the two-predicate nesting makes exactly three
   inhabited cells, the partition is canonical, and the derived W reaches
   all three;
3. PER-CELL QUANTUM FORCED: the top-generation torsion IS `W`, maximal,
   attained in every cell;
4. OFFSET FORCED: twice the derived channel reach, the maximum over every
   coupled-species assignment, with the banked-offset identity;
5. MULTIPLIER AND FORM FORCED: `M * W = 51 => M = 3`, and
   `cells * 17 + 2p = 55` solvable only at `p = 2`;
6. COUPLING FORCED: the weak-doublet perfect matching, both
   universalities, the constant charge step, the SM weak-isospin pattern,
   the neutrino leg, and the coincidence with the old declarations;
7. DECOYS EXCLUDED, derived form: the cell reading (57), every three-class
   reach, the cell-vs-channel confusion, the W2 `5 x 11` reading, the
   fourth cell, and the sub-maximal species readings;
8. FALSIFIERS: decoupling is exactly partnerlessness, for both carriers;
9. THE C12 DISCRIMINATOR AND BASE RULE: `+6` unreachable, the two-class
   bound, the canonical base rule closed;
10. THE AMPLITUDE EXPONENT, DERIVED: `55 - 13 = 42`. -/
theorem yardstick_premise_free_certificate :
    (Anchor.r0 Anchor.Sector.Electroweak = derivedEWYardstick
        ∧ derivedEWYardstick = 55)
    ∧ (cellReach derivedWCouples = 3
        ∧ (∃ f : Fermion, couplesToCharge f = true ∧ couplesToColor f = true)
        ∧ (¬ ∃ f : Fermion, couplesToColor f = true ∧ couplesToCharge f = false)
        ∧ (∀ c : SpeciesCell, couplesCellB derivedWCouples c = true)
        ∧ (∀ f : Fermion, cellOf f = SpeciesCell.quark ↔
            (couplesToCharge f = true ∧ couplesToColor f = true)))
    ∧ (Integers.tau 2 = (Anchor.W : ℤ)
        ∧ (∀ c : SpeciesCell, ∃ f : Fermion, cellOf f = c ∧ (genOf f).val = 2)
        ∧ (∀ g : Fin 3, Integers.tau g.val ≤ Integers.tau 2))
    ∧ (channelReach derivedWCouples = 2
        ∧ channelReach derivedZCouples = 2
        ∧ (∀ S : Fermion → Bool, channelReach S ≤ channelReach derivedWCouples)
        ∧ Anchor.r0 Anchor.Sector.Electroweak - 3 * (Anchor.W : ℤ)
            = 2 * channelReach derivedWCouples)
    ∧ ((∀ M : ℤ, M * (Anchor.W : ℤ)
          = derivedEWYardstick - 2 * channelReach derivedWCouples → M = 3)
        ∧ (∀ p : ℤ, 1 ≤ p → p ≤ 3 →
            ((∃ cells : ℤ, cells * 17 + 2 * p = 55) ↔ p = 2)))
    ∧ ((∀ f : Fermion, derivedWCouples f = true)
        ∧ (∀ f : Fermion, derivedZCouples f = true)
        ∧ (∀ f : Fermion, (allFermions.filter fun g => weakDoubletPartner f g).length = 1)
        ∧ (∀ f g : Fermion, weakDoubletPartner f g = true →
            tildeQ f - tildeQ g = 6 ∨ tildeQ f - tildeQ g = -6)
        ∧ (weakCharge .u = 1 ∧ weakCharge .c = 1 ∧ weakCharge .t = 1
            ∧ weakCharge .nu1 = 1 ∧ weakCharge .nu2 = 1 ∧ weakCharge .nu3 = 1
            ∧ weakCharge .d = -1 ∧ weakCharge .s = -1 ∧ weakCharge .b = -1
            ∧ weakCharge .e = -1 ∧ weakCharge .mu = -1 ∧ weakCharge .tau = -1)
        ∧ (weakDoubletPartner .nu1 .e = true ∧ weakDoubletPartner .nu2 .mu = true
            ∧ weakDoubletPartner .nu3 .tau = true)
        ∧ (∀ f : Fermion, GaugeCarrier.couples .wBoson f = derivedWCouples f)
        ∧ (∀ f : Fermion, GaugeCarrier.couples .zBoson f = derivedZCouples f))
    ∧ (3 * (Anchor.W : ℤ) + 2 * cellReach derivedWCouples = 57
        ∧ (∀ S : Fermion → Bool, (57 : ℤ) ≠ 3 * (Anchor.W : ℤ) + 2 * channelReach S)
        ∧ cellReach derivedWCouples ≠ channelReach derivedWCouples
        ∧ (derivedEWYardstick - 2 * channelReach derivedWCouples)
            % (Anchor.E_passive : ℤ) ≠ 0
        ∧ 4 * (Anchor.W : ℤ) + 2 * channelReach derivedWCouples ≠ derivedEWYardstick
        ∧ (3 * (Anchor.W : ℤ) + 2 * activeChannelClasses Fermion.e
              ≠ Anchor.r0 Anchor.Sector.Electroweak
            ∧ 3 * (Anchor.W : ℤ) + 2 * activeChannelClasses Fermion.nu1
              ≠ Anchor.r0 Anchor.Sector.Electroweak))
    ∧ ((∀ f : Fermion, derivedWCouples f = false ↔
          ∀ g : Fermion, weakDoubletPartner f g = false)
        ∧ (∀ f : Fermion, weakCharge f = 0 ↔ derivedWCouples f = false))
    ∧ ((∀ f : Fermion, 2 * activeChannelClasses f ≠ 6)
        ∧ (∀ f : Fermion, activeChannelClasses f ≤ 2)
        ∧ (∀ f : Fermion,
            (⟨1, le_refl 1⟩ : DofPricing).exponentOf
                canonicalChannelModel.distinctionsPerChannel
              * activeChannelClasses f = 2 * activeChannelClasses f))
    ∧ (derivedEWYardstick - 13 = 42 ∧ derivedEWYardstick - 5 - 8 = 42) :=
  ⟨⟨anchor_r0_ew_eq_derivedEWYardstick, derivedEWYardstick_eq_55⟩,
   ⟨cellReach_derived_w, three_cells_inhabited.1, no_color_active_charge_inactive,
    derived_w_touches_all_cells, fun f => (cell_iff_predicates f).1⟩,
   ⟨third_generation_torsion_eq_W, cell_has_third_generation,
    top_generation_torsion_is_max⟩,
   ⟨channelReach_derived_w, channelReach_derived_z, channelReach_derived_maximal,
    ew_offset_eq_twice_derived_channel_reach⟩,
   ⟨multiplier_forced_three_derived, form_rigid_in_predicates⟩,
   ⟨derived_w_universal, derived_z_universal, doublet_partner_unique,
    doublet_charge_step_of_partner, weakCharge_sm_pattern,
    ⟨neutrino_leg_forced.1, neutrino_leg_forced.2.1, neutrino_leg_forced.2.2.1⟩,
    declared_w_eq_derived, declared_z_eq_derived⟩,
   ⟨cell_reading_yields_decoy_derived, decoy_ne_twice_boson_channel_reach,
    cellReach_derived_ne_channelReach_derived, five_e_passive_incompatible_derived,
    fourth_cell_would_break_yardstick_derived,
    submaximal_species_readings_miss_ew_yardstick⟩,
   ⟨w_decouples_iff_no_partner, weakCharge_eq_zero_iff_decoupled⟩,
   ⟨twice_channel_count_ne_six, activeChannelClasses_le_two, base_rule_canonical⟩,
   ⟨derived_exponent_decomposition.2, derived_exponent_decomposition.1⟩⟩

What this page does not claim

The theorem does not prove that the electroweak yardstick equals 55. The theorem does not establish the values of the cell reach or channel reach. The theorem makes no claim about measured particle masses or experimental data.

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/T10YardstickPremiseFreeCert.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