conservation_necessity_status
plain-language theorem explainer
Human-readable completion badge for the conservation-necessity chain: every named lemma from MP to existence of a non-trivial conserved flow is marked PROVEN, with no holes. Auditors and framework maintainers cite it when checking that the old distinguishability axiom can be retired. The body is pure string concatenation of status lines, not a mathematical argument.
Claim. A fixed status string reporting that the conservation-necessity formalization is complete: the recognition-event structure is defined; Meta-Principle implies recognition is meaningful; every non-trivial discrete event system admits recognition events; MP forces existence of a non-trivial flow and of a distinguishable flow; and the top-level conservation-necessity theorem is proved. It records that the old axiom (every flow is non-trivial) may be replaced by the weaker, proved claim that a non-trivial flow exists.
background
The surrounding module derives non-trivial conservation from the Meta-Principle (MP), so that recognition_requires_distinguishability need not be an axiom. The chain is: MP makes recognition possible on non-empty types; recognition of $X$ from $Y$ needs $X \neq Y$; in a discrete event system that distinction is carried by non-zero flow; hence MP forces non-trivial conservation.
Upstream objects include several RecognitionEvent structures (positive ratio or positive state encoding a recognition fact), discrete event systems with evolution, flow-on-edges FlowFS, and predicates NonTrivialFlow and Distinguishable. The summary theorem conservation_necessity_proven states: given MP and a system with two distinct evolving events, there exists a non-trivial conserved flow. A sibling summary mp_forces_distinguishable_flow_exists weakens the old universal claim to mere existence of a distinguishable flow.
proof idea
Not a proof. The definition builds one multi-line String by concatenating fixed checklist lines (core argument formalized; structures defined; each named lemma marked PROVEN) plus a short note that the axiom can be replaced by existence of non-trivial flows. A trailing #eval prints the badge at elaboration time. No tactics or lemmas are applied inside the definition itself; mathematical content lives in the referenced theorems it lists.
why it matters
Closes the conservation gap documented in the module: non-trivial conservation is forced by MP rather than postulated. The status string is the human-facing certificate that conservation_necessity_proven, mp_forces_nontrivial_flow_exists, and mp_forces_distinguishable_flow_exists are all hole-free, so LedgerNecessity can drop the strong axiom in favor of existence. In Recognition Science terms, flow is information transfer during recognition; MP guarantees recognition can occur, hence non-trivial flows must exist. No downstream Lean declarations currently depend on this string; its role is verification bookkeeping and release hygiene for the Necessity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.