from
plain-language theorem explainer
This theorem asserts that seven independent axioms suffice to derive four substantive structural conditions on distinctions plus three definitional facts. Researchers building the Recognition Science foundation cite it to justify the logical basis for equality costs and primitive separations before deriving J-cost convexity or action principles. The argument is a direct mapping that invokes the independence of spatial semantics and coupled axes to translate each axiom into the required conditions.
Claim. Seven independent axioms imply four substantive structural conditions on distinctions together with three definitional facts.
background
The PrimitiveDistinction module defines Distinction as a primitive separation of entities, with equalityDistinction supplying the reflexive, symmetric, and irreflexive properties, equalityCost associating a nonnegative cost to equalities, and related facts such as identity_from_equality and non_contradiction_from_equality. Upstream results supply the independence notions: LNALSemantics.independent gives voxels that evolve without neighbor interaction, while RSCoupledAxis.independent requires that coupled axes are carried by distinct primitives. The module imports LogicAsFunctionalEquation, placing the result in the setting where distinctions are governed by functional equations rather than set-theoretic membership.
proof idea
The proof is a direct axiomatic mapping. It applies the definition of independent from LNALSemantics to eliminate interaction terms and the definition from RSCoupledAxis to enforce primitive separation, thereby producing the four structural conditions and three definitional facts without further lemmas or tactics.
why it matters
The result supplies the foundational bridge used by downstream theorems including actionJ_local_min_is_global, Jcost_convex_combination, hamilton_equations_from_EL, costRateEL_const_one, and SpeechIntelligibilityCert. It completes the step from seven axioms to the structural conditions required for the J-cost and composition laws in the Recognition Science chain, directly supporting the transition to energy conservation and least-action principles. It touches the open question of whether the full set of seven axioms can be stated without additional scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.