Masses Sector Dependent Torsion No Dim Reversing Vertex Face Bijection

The impossibility of a dimension-reversing bijection

A cube in three dimensions has 8 vertices, 6 faces, and 12 edges. A dimension-reversing bijection would be a one-to-one pairing that sends vertices to faces and faces to vertices, while respecting the incidence structure of the cube. The declaration no_dim_reversing_vertex_face_bijection in the Recognition Science library establishes, as a formal theorem, that no such bijection exists for a 3-dimensional cube.

The proof is a direct computation. The number of vertices is 8 and the number of faces is 6. A bijection between two finite sets requires them to have the same cardinality. Since 8 does not equal 6, no bijection, let alone one that reverses dimension, can exist. The declaration formalizes this elementary observation in the machine-checked library of formal theorems.

In Recognition Science, this fact appears in the derivation of particle mass generation. The framework models the generation of particle masses as a sequence of steps on a cube's cell counts. The relevant cell counts for the down quark sector are 6 faces and 8 vertices. The impossibility of a dimension-reversing bijection between these sets is part of the structure that forces the specific sequence of cell counts, rather than allowing a symmetric or reversible alternative.

The declaration does not claim that the assignment of the numbers 6 and 8 to the down quark sector is derived from first principles. That assignment is identified from experimental data and is a hypothesis. The theorem only establishes a mathematical property of the integers involved, not the physical reason why those integers are used.

theorem S0_at_D3 : S0 3 = 8 := by native_decide

theorem faces_at_D3 : cube_faces' 3 = 6 := by native_decide

What this page does not claim

The declaration does not claim that the assignment of the numbers 6 and 8 to the down quark sector is derived from first principles; that assignment is a hypothesis supported by data. The declaration does not claim that no bijection exists between vertices and faces in dimensions other than three. The declaration does not claim that the cube's cell counts are the only possible source of the particle mass generation steps.

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/SectorDependentTorsion.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: