jCost_before_arithmetic
plain-language theorem explainer
The pre-temporal forcing order places the J-cost stage before the arithmetic-object stage; researchers assembling the dependency chain from recognition primitives to arithmetic would cite this link; the proof is a one-line decidable rank comparison.
Claim. In the pre-temporal forcing order, the J-cost stage precedes the arithmetic-object stage: $rank(jCost) < rank(arithmeticObject)$.
background
The module records a forcing order among dependency stages that must be in place before physical time emerges. Stage is the inductive type listing the pre-temporal layers: distinction, recognitionInterface, singleValuedPredicate, symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick. Before is the relation rank a < rank b, equipped with a decidable instance. The local setting distinguishes recognition-light (primitive distinction) from physical light (downstream of J-cost and spacetime). The upstream jCost definition supplies the J-cost proxy used to name the stage.
proof idea
One-line wrapper that applies the decidable instance of Before via the decide tactic.
why it matters
This theorem supplies one link in the pre-temporal forcing chain that precedes the introduction of arithmetic objects; it sits between rcl_before_jCost and arithmetic_before_time in the sibling sequence and supports the overall order required by the Recognition Composition Law and J-uniqueness. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.