thirteen_natural_interpretations
plain-language theorem explainer
Thirteen admits three equivalent natural-invariant interpretations in the three-dimensional cube: as vertices plus faces minus body, as edges plus one, and as itself. Researchers tracing the Recognition Science mass ladder cite this when mapping generation steps to Q3 invariants. The proof reduces the conjunction to native arithmetic decisions via a refine tactic.
Claim. For the three-dimensional cube, $V + F - C = 13$, $E + 1 = 13$, and $13 = 13$, where $V, E, F, C$ denote the numbers of vertices, edges, faces, and the three-dimensional body.
background
The module narrows the open forcing step between proved Q3 cube invariants and their assignment as generation steps. SectorDependentTorsion already establishes that the values {13, 11, 6, 8} are cell counts on the three-dimensional cube at D=3, with the Euler characteristic χ(S²)=2 supplying the relations V-E+F=2 that rearrange to the two nontrivial identities for 13. Upstream results fix the discrete setting: RSNativeUnits sets c=1 and the phi-ladder, while CellularAutomata.step supplies the local rule that generates successor states on the recognition tape.
proof idea
The proof is a one-line term-mode wrapper. It refines the goal into the three conjuncts and discharges each arithmetic equality with native_decide.
why it matters
The theorem supplies the Euler identity for 13, which the module summary lists as newly proved and which supports the conditional uniqueness of the chain (13, 11, 6, 8) modulo the edge-symmetric filter. It advances the T8 step that forces D=3 and the identification of generation steps with cube invariants on the phi-ladder. The remaining openness, quoted from the module, is the physical reason the Up sector selects the edge-symmetric opening rather than another pair summing to 21.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.