axiom_summary
plain-language theorem explainer
The axiom_summary definition outputs a formatted string that tallies the axioms in the Recognition Science formalization by epistemic category. A researcher reviewing the formalization would cite it to obtain an immediate count of foundational claims versus open items. The definition is a direct string concatenation of four fixed lines with no lemmas or computation.
Claim. A string that reports the counts 4 physical postulates, 8 mathematical facts, 2 open problems, and total 14.
background
The Meta.Axioms module maintains a registry that classifies every axiom used in the formalization into three categories. Physical postulates are the minimal claims that define what physics is, such as the meta-principle and recognition exchange invariance. Mathematical facts are standard results accepted for pragmatic reasons, including ODE uniqueness for the cosh solution and convexity of cosh. Open problems are conjectures at the research frontier, such as the missing shift in the electron mass formula. The single upstream dependency is the Physical structure from Bridge.DataCore, which encodes positivity of the bridge constants c, ħ, and G.
proof idea
The definition is a direct string concatenation of the four category lines followed by the total line.
why it matters
This definition supplies the summary line that appears in the module documentation table of all 14 items. It flags the two open problems at the T9 frontier without resolving them. No downstream declarations depend on the string itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.