Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PublicSpine

show as:
view Lean formalization →

Curated public surface for Recognition Science foundation claims: strength-tagged packages for the forced tower, cost selection, phi-from-iota, circle H1, and linking encoding. Downstream cost-selection and linking-assembly modules import it as the only sanctioned entry point. Structure is packaging and holds-lemmas over T5–T8 and Alexander-duality bridges, not a single new derivation.

claimPublic spine of strength-tagged foundation packages: forced tower (unique $J$-cost from the recognition composition law, $\varphi$ as self-similar fixed point, continuum as purchase, floor demarcation), cost-selection package, $\varphi$ from $\iota$, nontrivial reduced $H^1(S^1)$, and linking-still-encoding. Untagged theorem badges are refused; each package is certified only under an explicit strength tag.

background

Recognition Science forces physics from one functional equation. The T5–T8 chain uniquely fixes the cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), the golden ratio $\varphi$ as self-similar fixed point, the eight-tick octave, and spatial dimension $D=3$. The Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ is the algebraic engine behind cost uniqueness.

Topologically, non-trivial circle linking in the $D$-sphere exists iff $D=3$ (Alexander duality / Hatcher 3.44), replacing the old tautology that simply defined linking as $D=3$. Upstream modules supply singular-simplex winding, Mathlib cohomology bridges for reduced $H^1(S^1)$, vanishing of linking detectors in $D=0,1$, and dimension-forcing arguments.

This module is the public surface of that stack. Its doc-line states the policy: strength-tagged claims only; untagged THEOREM badges are refused. Sibling objects (ForcedTower, CostSelectionPackage, PhiFromIota, floor demarcation, circle $H^1$, linking encoding) are the named packages consumers are allowed to cite.

proof idea

Aggregation and certification surface, not a fresh derivation. Imports pull FunctionalEquation helpers (T5), AlexanderDuality and DimensionForcing (T8 / $D=3$), CircleWindingChain and MathlibCohomologyBridge (homology invariant and reduced $H^1(S^1)$), LinkingVanishingLowDim (detector fails in $D=0,1$), PrimitiveRecognitionCalculus strength/delta, and the T6–T8 spine audit.

For each package the module defines a structure (tower, cost selection, phi-from-iota, floor demarcation, etc.) and a *_holds lemma that assembles upstream theorems under an explicit strength tag (Tagged). Continuum-as-purchase and linking-still-encoding are recorded as spine facts rather than re-proved here. Consumers should treat holds-lemmas as the API; raw upstream modules stay internal.

why it matters in Recognition Science

Single sanctioned public entry for foundation results that later layers must not re-import piecemeal. Used by PRCNativeCostSelection (native cost choice on the primitive recognition calculus) and PublicSpineLinkingAssembly (assembly of the linking side of the spine).

Closes the gap between internal forcing (T5 $J$-uniqueness, T6 $\varphi$, T8 $D=3$, RCL) and a referee-facing surface that only exposes strength-tagged packages. Without this gate, untagged theorem badges could leak definitional tautologies (e.g. linking defined as $D=3$) into downstream physics claims. Ties the topological linking argument and the cost/phi ladder into one audit path with T6T8SpineAudit.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.

declarations in this module (31)