Pith. sign in
module module moderate

IndisputableMonolith.Loom.CertificateData

show as:
view Lean formalization →

Concrete certificate payload for the Loom: basepoint, configuration pairs, bridge data, and automorphism tables encoding the homomorphism found by search on closed recognition walks. Separation witnesses and continuum residual analyses import these fixed tables rather than recomputing them. The module is data and definitions only; it does not prove correctness of the homomorphism.

claimFixed Loom certificate data: a basepoint, configuration pairs $(A,B)$ and $(C,D)$ with bridge records, and automorphism tables plus substitutions that encode the homomorphism discovered by search on the free group of rank $5$ of closed recognition walks (eight-state, three-axis window).

background

In the Loom, a recognition history is a walk on states; a finished history closes. On the eight-state, three-axis window forced by the chain (T7 eight-tick octave, T8 $D=3$), closed walks up to homotopy form a free group of rank $E-V+1=5$. A closed walk is thus a word in five signed generators, and a finished utterance is a finite list of such words sharing one basepoint.

Loom.Core supplies that certificate language. This module holds the concrete payload the search produced: named basepoint, configuration blocks, bridge data, and automorphism tables/substitutions that present the homomorphism relating those words. Downstream modules treat the tables as frozen inputs.

proof idea

This is a definition and data module, not a proof module. It binds named constants (basepoint, configuration pairs, bridge records, automorphism tables and substitutions) that package the homomorphism the search found. No lemmas are proved here; consumers import the bindings as fixed certificate material.

why it matters in Recognition Science

Separation imports the payload to check the kernel witness: every door has a key that opens it and one master key locks every door (versus the dual security-hole form). Continuum order-sensitive residual analysis (Campaign G4/G5) imports it when promoting finite Boolean non-membership in the metric edge image to a normalized-separation trichotomy under shape-regular refinement. The module therefore anchors both discrete Loom security checks and the continuum residual campaign to one shared homomorphism certificate rather than ad hoc tables.

scope and limits

used by (2)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)