pith. machine review for the scientific record. sign in
def definition def or abbrev

SelfConsistent

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 532def SelfConsistent (input_D output_D : ℕ)
 533    (input_vertices output_vertices : ℕ)
 534    (input_gen output_gen : ℕ) : Prop :=

proof body

Definition body.

 535  input_D = output_D ∧ input_vertices = output_vertices ∧ input_gen = output_gen
 536
 537/-- **THEOREM**: Recognition Science is self-consistent.
 538    The spectral analysis of R̂ on Q₃ reproduces D = 3, 8 vertices,
 539    and 3 generations — exactly the values used to construct R̂.
 540
 541    Input (construction): D = 3, V = 2^D = 8, gen = face_pairs = 3
 542    Output (spectral):    D = 3, V = 8, gen = 3  (from this module) -/

used by (1)

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

depends on (18)

Lean names referenced from this declaration's body.