Examples and distinctions
Constructed examples of this model; each answer includes the Lean statement.
Selected argument
Return to conclusion
Back
Meaning dependencies
Inference and proof references
Complete project specification
Exact root statement ∀ {NExperiment : Type uNExperiment} {NFrame : Type uNFrame} {NPlace : Type uNPlace} {NResult : Type uNResult}
(context :
PhysicsLogic.Paradigm.EquivalencePrinciples.LocalNongravitationalExperimentContext NExperiment NFrame NPlace
NResult),
context.LocalLorentzInvariance →
context.LocalPositionInvariance →
∀ (experiment : NExperiment) (firstPlace secondPlace : NPlace) (firstFrame secondFrame : NFrame),
context.nongravitationalExperiment experiment →
context.localAt experiment firstPlace →
context.localAt experiment secondPlace →
context.freelyFallingFrameAt firstFrame firstPlace →
context.freelyFallingFrameAt secondFrame firstPlace →
context.freelyFallingFrameAt secondFrame secondPlace →
context.relativelyUniformAt firstFrame secondFrame firstPlace →
context.experimentResult experiment firstFrame firstPlace =
context.experimentResult experiment secondFrame secondPlace
Compare two arguments
Compare their definitions and hypotheses. Shared declarations may be instantiated
differently; differences do not establish equivalence or implication.
Compared statement
No comparison No comparison argument selected.
Compare an earlier extraction
Compare the displayed specifications with an earlier JSON export.
This compares text, not mathematical equivalence. Files stay in this browser.
Earlier extraction
Clear comparison
No earlier extraction selected.
Notes and questions
Export notebook
Merge notebook
Import merges local entries without overwriting them.
All declarations in the selected argument
Find a declaration
Definitions, structures, and assumptions
Enable JavaScript to open the Lean code panel.
Structures, classes, and inductive alternatives
PhysicsLogic.Paradigm.EquivalencePrinciples.LocalNongravitationalExperimentContext structure
Definitions and domain choices
PhysicsLogic.Paradigm.EquivalencePrinciples.LocalNongravitationalExperimentContext.LocalLorentzComparisonScope definition PhysicsLogic.Paradigm.EquivalencePrinciples.LocalNongravitationalExperimentContext.LocalLorentzInvariance definition PhysicsLogic.Paradigm.EquivalencePrinciples.LocalNongravitationalExperimentContext.LocalPositionComparisonScope definition PhysicsLogic.Paradigm.EquivalencePrinciples.LocalNongravitationalExperimentContext.LocalPositionInvariance definition PhysicsLogic.Paradigm.EquivalencePrinciples.LocalNongravitationalExperimentContext.NonvacuousLocalLorentzInvariance definition PhysicsLogic.Paradigm.EquivalencePrinciples.LocalNongravitationalExperimentContext.NonvacuousLocalPositionInvariance definition PhysicsLogic.Paradigm.EquivalencePrinciples.LocalNongravitationalExperimentContext.experimentResult definition PhysicsLogic.Paradigm.EquivalencePrinciples.LocalNongravitationalExperimentContext.freelyFallingFrameAt definition PhysicsLogic.Paradigm.EquivalencePrinciples.LocalNongravitationalExperimentContext.localAt definition PhysicsLogic.Paradigm.EquivalencePrinciples.LocalNongravitationalExperimentContext.nongravitationalExperiment definition PhysicsLogic.Paradigm.EquivalencePrinciples.LocalNongravitationalExperimentContext.relativelyUniformAt definition PhysicsLogicConsumer.LocalInvariance.disconnected definition PhysicsLogicConsumer.LocalInvariance.response definition PhysicsLogicConsumer.LocalInvariance.unmatched definition
Checked statements: parameters, hypotheses, and interpretation
PhysicsLogic.Paradigm.EquivalencePrinciples.local_lorentz_and_position_invariance_transfer_between_available_frames checked statement PhysicsLogicConsumer.LocalInvariance.both_nonvacuous_clauses_iff_both_sensitivities_vanish checked statement PhysicsLogicConsumer.LocalInvariance.disconnected._proof_1 checked statement PhysicsLogicConsumer.LocalInvariance.disconnected._proof_2 checked statement PhysicsLogicConsumer.LocalInvariance.disconnected_scopes_satisfy_both_nonvacuous_clauses checked statement PhysicsLogicConsumer.LocalInvariance.lorentz_invariance_does_not_supply_position_invariance checked statement PhysicsLogicConsumer.LocalInvariance.lorentz_invariance_iff_no_orientation_sensitivity checked statement PhysicsLogicConsumer.LocalInvariance.occupied_locations_need_not_supply_a_matched_position_comparison checked statement PhysicsLogicConsumer.LocalInvariance.position_invariance_does_not_supply_lorentz_invariance checked statement PhysicsLogicConsumer.LocalInvariance.position_invariance_iff_no_position_sensitivity checked statement PhysicsLogicConsumer.LocalInvariance.scoped_invariances_do_not_compare_disconnected_laboratories checked statement PhysicsLogicConsumer.LocalInvariance.the_library_transfers_the_calibrated_response checked statement PhysicsLogicConsumer.LocalInvariance.the_response_has_both_comparison_scopes checked statement
Constructors, projections, and other meaning dependencies
PhysicsLogic.Paradigm.EquivalencePrinciples.LocalNongravitationalExperimentContext.mk constructor
External mathematical declarations
And external type boundary Bool external type boundary Bool.false external type boundary Bool.true external type boundary Decidable.decide external type boundary Eq external type boundary Exists external type boundary Fin external type boundary Fin.instOfNat external type boundary HAdd.hAdd external type boundary HMul.hMul external type boundary HPow.hPow external type boundary Iff external type boundary LE.le external type boundary Monoid.toNatPow external type boundary Nat external type boundary Nat.AtLeastTwo external type boundary Nat.instAtLeastTwoHAddOfNat external type boundary Nat.instNeZeroSucc external type boundary Ne external type boundary NeZero external type boundary Not external type boundary OfNat.ofNat external type boundary One.toOfNat1 external type boundary Prod external type boundary Prod.fst external type boundary Prod.mk external type boundary Real external type boundary Real.instAdd external type boundary Real.instLE external type boundary Real.instMonoid external type boundary Real.instMul external type boundary Real.instNatCast external type boundary Real.instOne external type boundary Real.instZero external type boundary True external type boundary Unit external type boundary Unit.unit external type boundary Zero.ofOfNat0 external type boundary Zero.toOfNat0 external type boundary instAddNat external type boundary instDecidableEqBool external type boundary instDecidableEqFin external type boundary instHAdd external type boundary instHMul external type boundary instHPow external type boundary instOfNatAtLeastTwo external type boundary instOfNatNat external type boundary ite external type boundary
Hughes-Robinson-Beltran-Lopez 1960, pp. 342-344, changes orientation relative to the galaxy and explicitly requires a suitable frequency reference; its finite upper bounds do not prove exact Lorentz invariance. Pound-Rebka 1960, pp. 337-341, compares radiation across a potential difference with thermal, calibration, and reversal qualifications, not identical local results in arbitrarily different frames. The scalar response and disconnected laboratory domains here are independent logical diagnostics, not either paper's measured data. They show independence of abstract clauses, not a counterexample to Schiff's conjecture under a specified dynamical theory.
Characterizations of the physical model