is
plain-language theorem explainer
The declaration defines the collision-free property for the assembled first-pass empirical program in Option A at the metadata layer. Researchers assembling Recognition Science schedules from queues and deliverables would cite it to confirm no overlaps in actions or pipelines. It is a direct class definition with zero proof lines that inherits completeness from sibling nodup and priority lemmas.
Claim. The first-pass empirical program satisfies collision-freeness: its actions, deliverables, and pipelines contain no duplicates and meet exact top-priority ordering.
background
The module supplies a single certificate that the first-pass empirical program attached to Option A is complete and collision-free at the metadata layer. It assembles prior results on queue, schedule, actions, deliverables, pipelines, and readiness into one object. Upstream, EdgeLengthFromPsi.is states that the result is either an algebraic tautology or a named hypothesis-discharge with zero sorry or axiom; MechanismDesignFromSigma.is constructs the n-agent combinatorial structure; MockThetaPhantom.is verifies an explicit structural analog in 8-tick neutrality.
proof idea
One-line class definition with empty proof body. It directly references the firstPassProgram construction together with the sibling facts firstPassProgram_nodup, firstPassProgram_deliverables_nodup, firstPassProgram_pipelines_nodup, and firstPassProgram_exact_top_priority.
why it matters
This supplies the collision-free certificate required by downstream acoustics results (optimalT60, hearingLossPenalty) and action results (energyConservationCert, christoffel, costRateEL_const_one) that apply J-cost. It closes the metadata layer of the Option A empirical program, consistent with the eight-tick octave and phi-ladder steps in the forcing chain. It leaves open the question of full physical embedding beyond metadata.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.