OneEquation

Structural consequences of the retraction equation at increasing levels of determination, machine-checked in Lean 4.

What this proves

One composition equation (fold after unfold = identity) forces a canonical carrier architecture on any computational model. The Lean code is the primary artifact; the companion paper provides motivation and interpretation.

At the pre-semantic level (RetractionModel, no grade function):

• fold_unfold_nonclosure. No FoldUnfoldSection exists from T(classicalRM) to classicalRM when headerLen > 0. Pure carrier geometry: fold shortens, unfold lengthens, contradiction by omega on length. Operates on RetractionModels, not GRMs.
• presemantic_not_group_C. selfApp ≠ id on the classical carrier when headerLen > 0. Carrier geometry only.

At the post-semantic level (GRM, grade = length):

• classicalGRM_factorsThrough. Self-application factors through headerLen. The cost is exactly achieved.
• construction_super_poly. The endomorphism count super-polynomially exceeds the description count. No polynomial covers the resource gap.

At the complexity level (P/NP on the characterized carrier):

• structural_bridge. Identity (rfl chain), structure (cross-pairing), and constraint (proved theorems) bundled.
• displacement_witnesses. Accept/reject conflation, 2-to-1 collapse, verification inputs displaced --- where selfApp acts on computational objects.

The conjunction (classical_carrier_structure) bundles the three main results for any positive-length header. classical_nonclosure instantiates at concreteHeader: no parameters, no hypotheses.

The obstruction is a property of the carrier, not of the P-NP relationship.

Project statistics

Metric	Value
Lean files	22 (9 Core, 7 Classical, 4 Complexity, 1 Cascade, 1 root)
Total lines	~4,300
Sorry count	0
Custom axioms	0
Lean 4 / Mathlib	v4.28.0

Type hierarchy

RetractionModel (carrier, fold, unfold, roundtrip)   -- pre-semantic, no grade
  GRM extends RetractionModel (+ grade)               -- adds semantics
    AdmissibleEncoding extends GRM (+ overhead)        -- computation model interface

FoldUnfoldSection (R1 R2 : RetractionModel)  -- weakest structural map, pre-semantic
Morphism / transportRM                        -- grade-free transport (RetractionModel)
Transport / transportGRM                      -- graded transport (GRM)

classicalRM : RetractionModel    -- classical carrier without grade
classicalGRM : GRM               -- classical carrier with grade = length
classicalAdmissibleEncoding      -- classical TM satisfies encoding interface

Build

lake build

Requires Lean 4 v4.28.0. Run lake build to fetch Mathlib and compile.

Determination levels

Results are stratified by what they require:

• Core (Tiers 0-4): Any retraction, any GRM, any carrier. The universal framework: idempotence, carrier architecture, transport, encoding invariance.
• Classical (Tiers 5-6): Carrier geometry determined (binary strings, fold = drop header, unfold = prepend header). Pre-semantic results (Tier 5) use classicalRM; post-semantic results (Tier 6) use classicalGRM with grade = length.
• Complexity (Tier 7): P and NP defined on the characterized carrier. Language = Set classicalGRM.carrier is definitional (rfl).
• Answer Space (Tier 8): Openness and conservation. Group C inhabited. Regime determined by headerLen.

Project structure

Core/ (9 files, Tiers 0-4) --- the universal framework, holds for any GRM:

• Primitives.lean (292) --- Retraction, RetractionModel, GRM, FullRetraction
• Regime.lean (145) --- regime predicates, classification, concrete models
• Transport.lean (141) --- transport model T(M), FoldUnfoldSection
• CarrierArchitecture.lean (453) --- carrier decomposition, naming layer, overflow confinement
• CertifyExtract.lean (223) --- projection, certify/extract asymmetry
• SplitIdempotent.lean (188) --- ReflectiveCarrierData = splitting of idempotent selfApp
• UniversalProperty.lean (341) --- carrier architecture unique up to unique isomorphism
• ReencodingInvariance.lean (413) --- BoundedGRMEquiv, encoding invariance, regime B invariance
• AdmissibleEncoding.lean (80) --- AdmissibleEncoding, SameSemantics, computation model interface

Classical/ (7 files, Tiers 5-6, 8) --- the classical determination:

• BinString.lean (86) --- binary string carrier, fold/unfold geometry
• CountingEngine.lean (134) --- N_Val, N_End, polynomial bounds
• Instantiation.lean (57) --- classicalRM, classicalGRM, classicalAdmissibleEncoding
• RegimeClassification.lean (41) --- classicalGRM is regime B
• Nonclosure.lean (54) --- fold_unfold_nonclosure
• Openness.lean (32) --- headerLen = 0 gives Group C
• CarrierCounting.lean (198) --- two-level naming gap, bounded asymmetry

Classical/Complexity/ (4 files, Tier 7) --- complexity on the carrier:

• StepBounded.lean (189) --- step-bounded computation, pair encoding
• Language.lean (135) --- P, NP, P subset NP
• CarrierConnection.lean (240) --- carrier identity, substrate iso, displacement theorems
• Parallel.lean (281) --- PNP structure, spectrum, structural bridge

Root:

• Cascade.lean (532) --- complete determination hierarchy (Tiers 0-8), oracle independence, non-vacuity witnesses, axiom audit
• OneEquation.lean (27) --- root import aggregator

Axiom profile

Every theorem uses only the standard Lean 4 kernel axioms: propext, Classical.choice, Quot.sound --- the same axioms Mathlib uses. Zero custom axioms. Core algebraic identities (idempotence, absorption, witness search) require zero axioms. The #print axioms calls in Cascade.lean verify axiom profiles at build time.

Verification

# Zero sorry
grep -r "sorry" OneEquation/ --include="*.lean" | grep -v STATUS
# Should return nothing

# Axiom audit (built into Cascade.lean)
lake build
# Check #print axioms output

Full theorem inventory

See CLAIMS.md for the complete theorem-by-theorem inventory with file locations, axiom profiles, and determination tiers.

License

Copyright (c) 2026 Larsen James Close. All rights reserved.