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 ∀ {Process : Type u} (readout : ChemicalTriangleFormulaReadout Process),
readout.SourceFormulaAt →
∀ (deltaA deltaB deltaC : ℝ),
deltaA + deltaB + deltaC = 0 →
HasDerivAt
(fun parameter =>
readout.idealFreeEnergyAt (readout.amountAValue + parameter * deltaA)
(readout.amountBValue + parameter * deltaB) (readout.amountCValue + parameter * deltaC))
(readout.freeEnergyVariationValueAt deltaA deltaB deltaC) 0
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.Papers.Onsager1931.ChemicalTriangleFormulaReadout structure
Definitions and domain choices
PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.EquationThreeEightAt definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.EquationThreeNineAt definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.EquationThreeSevenAt definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.EquationThreeTenAt definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.FormulaDomainAt definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.SourceFormulaAt definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.amountAValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.amountBValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.amountCValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.displacementAValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.displacementBValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.displacementCValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.displacementRateAValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.displacementRateBValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.displacementRateCValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.equilibriumAmountAValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.equilibriumAmountBValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.equilibriumAmountCValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.forceAValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.forceBValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.forceCValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.forceLawRatesAt definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.freeEnergyMinimumValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.freeEnergyValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.freeEnergyVariationValueAt definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.gasConstantValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.idealFreeEnergyAt definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.linearizedForceAt definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.logarithmicForceAt definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.massActionRatesAt definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.rateABValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.rateACValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.rateBAValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.rateBCValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.rateCAValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.rateCBValue definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.selectedProcess definition PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.temperatureValue definition PhysicsLogic.Papers.Onsager1931.ReciprocalRelationsFramework.Countermodels.PositiveChemicalRateLaw definition PhysicsLogic.Papers.Onsager1931.ReciprocalRelationsFramework.Countermodels.displacedChemicalTriangleFormula definition PhysicsLogic.Papers.Onsager1931.ReciprocalRelationsFramework.Countermodels.equilibriumChemicalTriangleFormula definition PhysicsLogic.Papers.Onsager1931.ReciprocalRelationsFramework.Countermodels.wrongChemicalTriangleFormula definition
Checked statements: parameters, hypotheses, and interpretation
PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.EquationThreeNineAt._proof_1 checked statement PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.a_common_force_shift_preserves_equation_three_eight checked statement PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.a_relative_displacement_cutoff_gives_a_uniform_force_error_tolerance checked statement PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.actual_free_energy_derivative_includes_the_number_change checked statement PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.equation_three_eight_retains_the_conserved_displacement checked statement PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.equation_three_nine_is_the_calibrated_logarithmic_force checked statement PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.equation_three_ten_conserves_total_displacement_rate checked statement PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.fixed_number_variations_remove_the_common_chemical_potential checked statement PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.forces_agree_on_conserved_variations_iff_they_differ_by_a_common_shift checked statement PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.linearized_forces_reproduce_the_mass_action_displacement_rates checked statement PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.relative_displacement_controls_relative_force_error checked statement PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.source_chemical_variation_is_the_actual_constrained_derivative checked statement PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.source_formula_retains_equations_three_seven_through_three_ten checked statement PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.source_formulas_use_the_actual_mass_action_rates checked statement PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.the_logarithmic_derivative_formula_is_exact_iff_total_variation_vanishes checked statement PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.the_logarithmic_force_error_is_quadratic_in_relative_displacement checked statement PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.the_logarithmic_force_has_the_printed_first_order_expansion checked statement PhysicsLogic.Papers.Onsager1931.DissipationFunctional.Countermodels.reciprocal._proof_1 checked statement PhysicsLogic.Papers.Onsager1931.DissipationFunctional.Data.dissipation._proof_1 checked statement PhysicsLogic.Papers.Onsager1931.ReciprocalRelationsFramework.Countermodels.a_named_chemical_rate_law_does_not_supply_equations_three_seven_through_three_ten checked statement PhysicsLogic.Papers.Onsager1931.ReciprocalRelationsFramework.Countermodels.absolute_displacement_does_not_control_the_force_error_uniformly checked statement PhysicsLogic.Papers.Onsager1931.ReciprocalRelationsFramework.Countermodels.arbitrarily_small_displacements_do_not_make_the_linearized_substitution_exact checked statement PhysicsLogic.Papers.Onsager1931.ReciprocalRelationsFramework.Countermodels.changing_total_amount_is_not_the_fixed_number_variation checked statement PhysicsLogic.Papers.Onsager1931.ReciprocalRelationsFramework.Countermodels.constrained_variations_do_not_select_the_absolute_logarithmic_forces checked statement PhysicsLogic.Papers.Onsager1931.ReciprocalRelationsFramework.Countermodels.substituting_exact_forces_leaves_a_computed_rate_residual checked statement PhysicsLogic.Papers.Onsager1931.ReciprocalRelationsFramework.Countermodels.the_displaced_family_has_positive_source_data checked statement PhysicsLogic.Papers.Onsager1931.ReciprocalRelationsFramework.Countermodels.the_displaced_family_keeps_a_detailed_balanced_reference checked statement PhysicsLogic.Papers.Onsager1931.ReciprocalRelationsFramework.Countermodels.the_exact_force_substitution_error_is_strict_at_positive_displacement checked statement PhysicsLogic.Papers.Onsager1931.ReciprocalRelationsFramework.Countermodels.the_exact_force_substitution_still_agrees_to_first_order checked statement PhysicsLogic.Papers.Onsager1931.ReciprocalRelationsFramework.Countermodels.the_positive_chemical_reference_realizes_the_constrained_source_formulas checked statement PhysicsLogic.Papers.Onsager1931.ReciprocalRelationsFramework.Countermodels.the_source_rate_law_reproduces_the_actual_displaced_kinetics checked statement
Constructors, projections, and other meaning dependencies
PhysicsLogic.Papers.Onsager1931.ChemicalTriangleFormulaReadout.mk constructor