neutron_discrepancy_implies_lifetime_input
The result shows that the neutron lifetime discrepancy derived from the ledger directly supplies the neutron lifetime input placeholder. Experimental groups reconciling beam versus bottle neutron lifetime measurements would cite this when mapping observed discrepancies onto Recognition Science ledger conditions. The proof is a one-line term that returns the hypothesis unchanged.
claimIf the neutron lifetime discrepancy is obtained from the ledger, then the neutron lifetime input from the ledger holds, where the input asserts neutron decay charge $Q > 0$ and positive free neutron mean lifetime.
background
Recognition Science treats neutron lifetime via structural placeholders rather than explicit formulas. The definition neutron_lifetime_from_ledger requires neutronDecayQ > 0 and freeNeutronMeanLife > 0, serving as a minimal ledger condition for decay processes. The companion definition neutron_lifetime_discrepancy_from_ledger is set equal to this same proposition, creating an experimental interface in the NeutronLifetimeDiscrepancyStructure module.
proof idea
The proof is a term-mode identity: the hypothesis h is returned directly. Because neutron_lifetime_discrepancy_from_ledger is definitionally identical to neutron_lifetime_from_ledger, the implication holds by reflexivity with no additional lemmas required.
why it matters in Recognition Science
The declaration supplies the minimal bridge that lets experimental neutron lifetime data enter the Recognition Science ledger without extra hypotheses. It sits downstream of the Nuclear.NeutronLifetimeStructure placeholder and upstream of any future reconciliation of the neutron lifetime anomaly with the phi-ladder mass formula. No downstream uses are recorded, leaving its role in full T5-T8 chain applications open.
scope and limits
- Does not derive a numerical value for the neutron mean life.
- Does not quantify the size of any experimental discrepancy.
- Does not invoke the J-cost function or phi-ladder rung assignments.
- Does not address the eight-tick octave or spatial dimension forcing.
formal statement (Lean)
19theorem neutron_discrepancy_implies_lifetime_input
20 (h : neutron_lifetime_discrepancy_from_ledger) :
21 neutron_lifetime_from_ledger :=
proof body
Term-mode proof.
22 h
23
24end NeutronLifetimeDiscrepancyStructure
25end Experimental
26end IndisputableMonolith