Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Strength

show as:
view Lean formalization →

Defines the strength tag that grades Primitive Recognition Calculus claims by how much structure they assume: pure discrete delta, choice, or full trace closure. Downstream PRC modules and the public dual spine import it to keep delta-only results from being mislabeled as continuum theorems. The module is mostly inductive tags plus inequality lemmas separating the grades.

claimA strength tag for a PRC claim is one of three grades: $\delta$-only (discrete tower $\mathbb{N}/\mathbb{Z}/\mathbb{Q}$), choice-dependent, or trace-closure (continuum-level). The module records that these grades are pairwise distinct, so a $\delta$-only certificate is never silently read as a trace-closure theorem.

background

Primitive Recognition Calculus (PRC) is the foundation layer that packages Recognition Science forcing statements before they are exposed on the public dual spine. Claims in that layer are not all equally strong: some live entirely on the discrete $\delta$-tower, some invoke classical choice, and some require trace closure into the continuum.

This module introduces the strength tag (panel K1) that labels each such claim. The PublicSpine documentation states the policy explicitly: the $\delta$-only tower covers $\mathbb{N}/\mathbb{Z}/\mathbb{Q}$ via forced_tower_holds, while continuum cuts sit under classical extension and must not be filed under $\delta$-only. Strength is the bookkeeping type that enforces that separation.

Sibling names in the module include the tag type itself, a claim wrapper carrying a tag, and inequality lemmas asserting that $\delta$-only is not trace closure and that choice is not $\delta$-only.

proof idea

This is primarily a definition module: an inductive (or enumerated) strength tag, a claim record pairing a proposition with its tag, and short decidable inequalities between constructors. The inequality lemmas are constructor-discrimination proofs, not deep analytic arguments. No forcing-chain algebra is proved here; the module only supplies the stratification vocabulary used elsewhere.

why it matters in Recognition Science

Without an explicit strength tag, delta-only tower results can be misread as continuum theorems. PublicSpine is the dual forcing surface opposite UnifiedForcingChain; it imports this module so the honest $\delta$-stratified map can refuse to place $\neg\mathbb{R}$ under $\delta$-only (panel K2). Basic, Kernel, RealCompletion, and TraceClosure all import Strength so every PRC claim carries a grade before it is assembled into the public spine.

In the broader Recognition framework this is bookkeeping for the forcing chain (T0–T8), not a replacement for J-uniqueness, $\varphi$, the eight-tick octave, or $D=3$. It keeps the discrete certificates pedagogically and formally separate from classical continuum extensions.

scope and limits

used by (5)

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

declarations in this module (4)